\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}  		
\usepackage[danish]{babel}
\usepackage{enumerate}
\usepackage{graphicx}

\usepackage{listings} 

\title{Videnskabsteori 2009 -- Synopsis\\case: Hvornår er et bevis et bevis?}
\author{Rasmus Erbou Røge \& Troels Bak Andersen}
\date{\today}

\usepackage{fancyhdr}
\fancyhf{}
\pagestyle{fancy}
\lhead{\bfseries Videnskabsteori 2009} 
\chead{} 
\rhead{case: Hvornår er et bevis et bevis?} 
\lfoot{} 
\cfoot{} 
\rfoot{\thepage} 
\renewcommand{\headrulewidth}{0.4pt} 
\renewcommand{\footrulewidth}{0.4pt} 
\fancyheadoffset{0.04pt}

\begin{document}
\maketitle
% -- Note --
%Brug dette afsnit til tekniske beskeder til hinanden.
%Rasmus, jeg får ikke skrevet mere på synopsen for i dag. Det du skal gøre er, at få læst min behandling af Heintz igennem. Jeg er bange for, jeg har bevæget mig lidt for langt væk fra spørgsmålet, jf. min kommentar i linie 67. Så skal du sammenligne det syn Heintz har på matematikere med Platons... Jeg synes slet ikke den sammenligning har relevans i forhold til det, jeg har skrevet indtil videre, så jeg håber du kan få noget fornuftigt ud af det. Så skal du behandle hele Hannas tekst, den har jeg slet ikke skrevet noget til. Jeg er dog kommet med nogle overordnede kommentarer til den. Jeg har heller ingen input til diskussionen til sidst.
%Troels, jeg har ikke nogle beskeder til dig endnu...


% -- Tanker --
%Opgaven skal opbygges som sammenhængende tekst, men det skal være oplagt, at den er delt ind i redegørelse, analyse og til sidst diskussion. Vi kan overveje, om teksten skal deles ind i overskrifter.

% -- Introduktion --
%En kort beskrivelse af hvad vi vil fortælle om i vores synopsis. 



% -- Redegørelse --

%En sætning i stil med: "Jeg vil først redegøre for ... Dernæst vil jeg analysere ... ved at sammenholde ... Dette leder frem til en diskussion af ... til hvilken jeg endvidere inddrager ..."

%Hvem er Betina Heintz, og hvordan forholder hun sig professionelt til MacKenzie?
Betina Heintz er sociolog og forsker i matematikeres opfattelse af bevisers rolle i teoretisk matematik. Derved er det nærlæggende for hende at anmelde Donald MacKenzies bog, der omhandler samme emne inden for datalogien. 

%Repeter Devlins to fløje af beviser:
%- højrefløjens formelle beviser og
%- venstrefløjens bevis ved international konsensus.
Vi genkalder os de to fløje af matematiske beviser som illustreret i \cite{devlin}, nemlig højrefløjens formelle bevisførelse og venstrefløjens bevis ved international konsensus. Det er væsentligt her at bemærke, at vi her snakker om beviser for teoretisk matematik, det Heintz omtaler som \emph{pure mathematics}. 

Temaet i MacKenzies bog er kulturen for bevisførelse i anvendt matematik, nærmere betegnet programmering som beskrevet i \cite[afsnit 2.4]{noter}. Han forsøger inden for dette emne at beskrive hvori bevisførelsen for korrektheden af et program består. Heintz perspektiverer dette syn på beviser til sin egen undersøgelse af, hvad bevisets rolle er i teoretisk matematik.

%Hvem er Gila Hanna? 


% -- Analyse --

%MacKenzie behandler formel bevisførelse for korrektheden af computerprogrammer og karakteriserer to typer beviser i stil med Devlin (s. 930 øverst):
%- check ved empirisk efterprøvning eller ved
%- matematisk bevisførelse.
%Senere (s. 937) deler han formel mekanisk bevisførelse ind i to afdelinger:
%- formelle beviser og
%- stringente (rigorous) beviser
%Er der virkelig en forskel? Er det en væsentlig diskussion i artiklen?
Der skitseres forskellige opfattelser for et bevis af korrektheden af et program \cite[s. 930 nederst]{heintz}. Disse inkluderer fuldstændigt mekaniserede beviser med eller uden hjælp fra en computer, fuldstændigt formaliserede beviser udført \emph{i hånden} af matematikere og beviser, der giver andre matematikere indsigt i programmets korrekthed. Vi skal her se de to første typer som analogt med de formalistiske matematiske beviser, og den sidste analogt med bevis ved konsensus. 

Det er dog ikke helt ligetil, hvad Heintz mener adskiller de to første typer fra hinanden. Begge typer beviser er formelle, men et bevis af den første type er aksiomatiseret, således at det mekanisk kan gennemlæses. Her opstiller MacKenzie kriterier for en sådan aksiomatisering \cite[s. 932 øverst]{heintz}, og snakker herefter om hvordan man kan konstruere automatiserede sætningsbevisere. Den væsentlige forskel er her dog, at de lange og besværlige udregninger bliver udført af en computer, som MacKenzie regner for mere pålidelig end mennesker \cite[s. 932 øverst, s. 937 midt]{heintz}. 
%Rasmus, jeg er bange for disse to afsnit blev for lange, og at det slet ikke er det, vi skulle fokusere på. Henrik skrev jo selv, at vi skulle fokusere på konklusionen s. 937-9.

%De to følgende afsnit hører måske inde under diskussionen.
Dette giver dog det nye problem, at gyldigheden af det skrevne program nu afhænger af gyldigheden af meta-programmet. Her giver MacKenzie den eneste løsning, at matematikere må bevise gyldigheden af meta-programmet i hånden \cite[s. 936 midt]{heintz}. Her nævner Heintz selv, at denne løsning er uholdbar, idet det kan være uoverskueligt at læse koderne i meta-programmet igennem. 

%På side 934-5 behandles sammenspillet mellem formel bevisførelse og virkeligheden. Formelle beviser kan kun bevise rigtigheden af en matematisk model, men ikke garantere, at et program virker efter hensigten.
Et andet centralt problem der påpeges er, at man ved formel verificering kun kan bevise korrektheden af den matematiske model bag et program, men ikke at programmet rent faktisk realiserer denne. 

%Skriv noget om, at inden for programverificering er man mere tilbøjelig til at stole på gyldigheden af programmer, der er formelt verificeret end programmer hvis korrekthed er forståelige for andre matematikere. Dette er nemlig det modsatte end normen inden for teoretisk matematik.
I den anden fløj af bevisførelse inden for datalogien er den uformelle, hvor der lægges vægt på, at argumenterne i en program verificering er forståelige for andre matematikere. Det nævnes i \cite[s. 937 midt]{heintz}, at denne retning ikke er særlig udbredt, hvorimod den analoge uformelle bevisførelse i matematikken er næsten den eneste anvendte. Det er denne diametrale forskel i anvendelse, Heintz snakker om, når hun i konklusionen af anmeldelsen nævner, at program verifikation har udviklet sin egen kultur i bevisførelse. 

%Skriv noget om, at Heintz's egen forskning viser, at bevisførelse faktisk ikke er den vigtigste part for teoretiske matematikere (s. 937-8). Dette er kun det sidste skridt i en større proces, hvor forståelse af matematikken er den væsentlige motivation. Kom her ind på Heintz's diskussion af forskellen på at forstå og bevise sætninger s. 938. 
Hun forklarer, at årsagen til denne forskel er at finde i processen af udviklingen af matematiske resultater. Hun påpeger, at den matematiske proces er mere rettet på at formidle forståelse for resultaterne, og at egentlig bevisførelse blot er den sidste afsluttende fase. Derimellem foregår en større eksperimentering med eksempler og fornemmelser, som stemmer helt overens med Lakatos's syn på den matematiske proces \cite{davis}.

I afslutningen på redegørelsen for de forskellige bevistyper og motivationen for at bruge dem blandt deres tilhængere giver hun MacKenzies egen mening: Det er op til det matematiske samfund at beslutte, hvilken type af argumenter der skal tælle som et bevis. %Igennem hele teksten, men specielt i konklusionen omkring midt side 938, skinner hendes begejstring for det uformelle bevis igennem. Da det er hendes egen konklusion er det usikkert, hvorvidt også MacKenzie hælder til denne bevistype. 

%Her skal vi komme ind på, hvordan synes på matematikken har ændret sig i løbet af tiden.
%[DET HER HAR INTET MED MACKENZIE AT GØRE]

I Heintzs konkluderende afsnit i \cite[s. 937]{heintz} kommer hun ind på, hvilken rolle beviset har for de forskellige grupperinger: 

Hos begge grader af formelle beviser fokuseres der på, at man opnår den højest mulige tillid til det beviste. Hun antyder desuden i \cite[s. 148 midt]{heintz}, at det formelle bevis giver mulighed for at bevise noget, der ikke er helt forstået. Det formelle bevis bliver, på trods af det typisk er ulæseligt, det helt centrale i matematikken. 

Det kommer til at stå i stærk modsætning til, for at bruge Devlins' ordbrug, venstrefløjsbeviser. Her bliver beviset nærmere en konklusion på alt det vigtige, et tjek der afslutter et stykke matematisk arbejde. Det viser sig i bl.a. i hendes citat af Michael Atiyah, der siger at beviset kun er som et sidste tjek i den process det er at lave matematik. Her er en del af bevisets rolle dog stadig at skabe tillid til matematikken, men det kommer på et tidspunkt i processen hvor der allerede er en stor grad af tillid. 

I begge bevistyper er en del af bevisets rolle at skabe tillid til sætningen og dermed til den matematik der bygger på den. Men der er store forskelle hvori den tillid man har til beviset er. I tilfældet med formelle beviser er tilliden bygget ind i beviset, da det blot er en lang række logiske udsagn. Det medfører at sætningen følger mekanisk logisk ud fra aksiomerne. 

I det uformelle tilfælde er det ikke helt så simpelt. Her finder vi grunden til tilliden i en matematisk konsensus om bevisets rigtighed, men hvordan opstår denne konsensus? Det er ikke noget Hertz berører særligt meget, men istedet kan vi inddrage Lakatos' syn fra \cite{davis}. Her fremkommer beviset og dermed tilliden via en dialektisk process mellem matematikere der langsomt former matematikken og løbende i processen vurderer korrektheden af slutninger. 

Et helt andet syn på hvorfor vi kan have tillid til matematiske sætninger finder vi hos Platon. For Platon er matematisk viden noget vi er født med og 'bare' skal genlære. I 'Menon' har han en dialog med en slave, der har det formål at belyse denne opfattelse. Han stiller en slave en lang række spørgsmål og får på den måde slaven til at forklare Menon og Sokrates et stykke, for slaven, ukendt matematik (ved at tage diagonalen i et kvadrat kan fremstilles et nyt kvadrat med det dobbelte areal). Så her virker det til, at tilliden til matematikken nærmest er indgroet og udelukkende kræver at man 'husker rigtigt'. 

Et andet aspekt Heintz har med i sin boganmeldelse er den historiske udvikling i hvad man anser for et bevis. Heintz skriver i \cite[s. 938 nederst]{heintz}, det først er i det 19. århundrede man er begyndt at kræve et stringent bevis for matematiske sætninger. Indtil da har de accepterede metoder og kravene til et 'stringent' ændret sig løbende. 

Vi har set hvordan Heintz introducerer to forskellige formelle bevistyper, men også at begge medfører store problemer. I den ene lejr bliver beviser uforståelige og får udelukkende den egenskab at vise noget med størst mulig sikkerhed. I den anden lejr bliver basen for et bevis' gyldighed en konsensus blandt matematikere, hvilket medvirker til at gøre dem fejlbarlige og tidsafhængige. 

Helt naturligt er det, at holde de forskellige bevistyper op mod hinanden. Hvilken skaber mest tillid til resultatet, hvordan er de i det daglige arbejde som matematiker og hvordan stemmer de overens med de krav vi har fået indarbejdet til beviser? 



%Hvordan skal der perspektiveres til Platon her. Vi skal sammenligne dette syn på matematisk evne med Heintz's. 

%Hanna fremsætter to former for bevisførelse (s. 6-8):
%- teoretiske (formelle) beviser og
%- forklarende beviser.
%Hun forklarer at de er præcis lige gyldige, og konkluderer at forklarende beviser bør begæres mere i det matematiske samfund.

%På s. 12 introducerer hun begrebet "overbevisende" bevis. Hun argumenterer for at det ikke er beviser, der skal motiveres.
%Hun gør en pointe ud af, at adskille fra dem fra de forklarende. Man kan sagtens være overbevist om en sætnings rigtighed uden at forstå hvorfor. Yderligere kan man også være overbevist om en sætnings rigtighed uden at den er sand.

%Dette kan opsummeres i: Hvordan adskiller man et overbevisende bevis fra et forklarende?
%Er dette et argument for at formelle beviser er nødvendige alligevel? Dette skal måske flyttes til diskussionen.

%Hun roder dog lidt rundt i sin notation: \begin{quote}But the focus of an explanatory proof is clearly upon understanding, rather than upon the deductive mechanism\end{quote}


% -- Diskussion --

%Hvad synes vi om Heintz's og MacKenzies argumenter?
%Hvordan kommer det til udtryk, at Heintz er sociolog?

%Hvordan spiller Hannas to bevis-roller sammen med nuværende forskning og undervisning i matematik?


% -- Literatur --

%Henvis til en kilde med \cite[s. 934]{heintz}

\begin{thebibliography}{Davis og Hersh}
\bibitem[Heintz]{heintz}
Bettina Heintz.
"When is a Proof a Proof?",
\emph{Social Studies of Science}
33.6 (dec. 2003).

\bibitem[Hanna]{hanna}
Gila Hanna.
"Some Pedagogical Aspects of Proof",
\emph{Interchange}
21.1 (1990).

\bibitem[Sørensen]{noter}
Henrik Kragh Sørensen.
"Noter til matematikkens videnskabsteori 2009",
\emph{Aarhus Universitet}
2009.

\bibitem[Devlin]{devlin}
Keith Devlin.
"When is a proof?",
\emph{Devlin's Angle}
(jun. 2003).

\bibitem[Davis og Hersh]{davis}
Philip J. Davis og Reuben Hersh.
"Lakatos and the Philosophy of Dubitability",
\emph{The Mathematical Experience}
(1981).
\end{thebibliography}

\end{document}
